E:Type, T, V:(IdIdType), M:(IdLnkIdType), pred?:(E(E+Unit)),
info:(E(IdId+(IdLnkE)Id)), init:(i,x:IdT(i,x)),
Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(x:IdT(i,x))),
val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) )).
(e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 SWellFounded(pred!(e;e'))
 (e:E. when-after(e;info;pred?;init;Trans;val)  (x:IdT(loc(e),x))(x:IdT(loc(e),x))) 

latex

Definitions

, x:A. B(x), P  Q, AB, t  T, x:AB(x), x:AB(x), Id, loc(e), when-after(e;info;pred?;init;Trans;val), f(a), n-m, n+m, -n, #$n, ij, pred!(e;e'), b, first(e), Prop, s = t, pred(e), kind(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), x. t(x), x,y. t(x;y), left+right, Unit, IdLnk, Type, SWellFounded(R(x;y)), x:A. B(x), , A, False, Void, a<b, {x:A| B(x) }, P  Q, P & Q, , b, <a,b>, x.A(x), P  Q, A & B, rcv?(e), sender(e), let x = a in b(x), S  T, Atom$n, s ~ t, SQType(T), {T}, S  T

Lemmas

Id sq, sender wf, rcv? wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, nat wf, le wf, Id wf, IdLnk wf, unit wf, kindcase wf, Knd wf, loc wf, kind wf, pred wf, first wf, assert wf, not wf, pred! wf, strongwellfounded wf, nat properties, ge wf